package phantm.dataflow

import phantm.Settings
import phantm.phases.PhasesContext
import phantm.cfg.{ LabeledDirectedGraphImp, VertexImp }
import phantm.types.TypeEnvironment
import phantm.cfg.Trees.Statement
import phantm.types.TypeEnvironment

class AnalysisAlgorithm(transferFun: TransferFunction[TypeEnvironment, Statement],
  bottomEnv: TypeEnvironment,
  baseEnv: TypeEnvironment,
  cfg: LabeledDirectedGraphImp[Statement],
  var facts: Map[VertexImp[Statement], TypeEnvironment]) {
  
  type Vertex = VertexImp[Statement]

  def pass(transferFun: TransferFunction[TypeEnvironment, Statement]) = {
    for (v <- cfg.V) {
      for (e <- cfg.inEdges(v)) {
        // We ignore unreachable code
        if (facts(e.v1) != bottomEnv) {
          transferFun(e.lab, facts(e.v1))
        }
      }
    }
  }

  def detectUnreachable(transferFun: TransferFunction[TypeEnvironment, Statement]): List[Statement] = {
    var res: List[Statement] = Nil;

    for (v <- cfg.V if v != cfg.entry) {
      if (cfg.inEdges(v).forall(e => (facts(e.v1) != bottomEnv) &&
        (transferFun(e.lab, facts(e.v1)) == bottomEnv))) {

        for (e <- cfg.outEdges(v)) {
          res = e.lab :: res
        }
      }
    }

    res
  }

  def computeFixpoint(ctx: PhasesContext): Unit = {
    var pass = 0;
    if (Settings.get.displayProgress && Settings.get.verbosity > 2) {
      println("      * Analyzing CFG (" + cfg.V.size + " vertices, " + cfg.E.size + " edges)")
    }

    facts = facts.updated(cfg.entry, baseEnv)

    var workList = Set[Vertex]();

    for (e <- cfg.outEdges(cfg.entry)) {
      workList += e.v2
    }
    while (workList.size > 0) {
      pass += 1

      if (Settings.get.displayProgress && Settings.get.verbosity > 2) {
        println("      * Pass " + pass + " (" + workList.size + " nodes in worklist)...")
      }

      val v = workList.head
      workList -= v
      val oldFact: TypeEnvironment = facts(v)
      var newFact: Option[TypeEnvironment] = None

      for (e <- cfg.inEdges(v) if facts(e.v1) != bottomEnv) {
        val propagated = transferFun(e.lab, facts(e.v1))
        if (propagated != bottomEnv) {
          newFact = newFact match {
            case Some(nf) => Some(nf union propagated)
            case None => Some(propagated)
          }
        }
      }

      val nf = newFact.getOrElse(oldFact.copy);
      if (nf != oldFact) {
        if (Settings.get.testsActive) {
          oldFact.checkMonotonicity(v, nf, ctx, cfg.inEdges(v) map (e => (e.lab, facts(e.v1))))
        }

        facts = facts.updated(v, nf)
        for (e <- cfg.outEdges(v)) {
          workList += e.v2;
        }
      }
    }
  }

  def dumpFacts = {
    for ((v, e) <- facts.toList.sortWith { (x, y) => x._1.name < y._1.name }) {
      println("  " + v + " => " + e)
    }
  }
  def getResult: Map[Vertex, TypeEnvironment] = facts
}
